COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∧I CVI_INDUCTION[PSI←λn.∀t.(length uuu(t) = n ∧ pc(t) = 1
C00004 ENDMK
C⊗;
∧I CVI_INDUCTION[PSI←λn.∀t.(length uuu(t) = n ∧ pc(t) = 1
 ∧ reverse1 uuu(t) * vvv(t) = reverse1 w
⊃ ∃t1.(t1 > t ∧ pc(t1) = 2 ∧ vvv(t1) = reverse1 w))];
ASSUME n=0;
ASSUME length uuu(t)=n∧(pc(t)=1∧(reverse1 uuu(t)*vvv(t))=reverse1 w);
∀e LENGTH_ZERO uuu(t);
tauteq uuu(t)=qNIL ↑↑↑:↑;
REWRITE ↑↑↑ BY LOGICTREE∪{ REVERSE1_NIL,APPEND_NIL,2,5};
REWRITE ↑↑↑↑ BY LOGICTREE∪{ REVERSE1_NIL,APPEND_NIL,LENGTH_NIL,2,5};
∀E ELEPHREV4 t;
EVAL ↑ BY { 5};
∧E ↑↑↑:#1;
EVAL ↑↑ BY {10};
∀E ELEPHREV3 t;
∧E 7:#2;
EVAL ↑↑ BY { 5,10,13};
REWRITE (t+1)>t BY NATNUMSS∪ARITHSS∪{ ONE};
∧I (15 11 14);
∃I ↑ (t+1)←t1;
⊃I 3⊃↑;
label n0;
⊃I 2 ↑;
assume ¬(n=0);
ASSUME ∀m.(m<n⊃∀t.((length uuu(t)=m∧(pc(t)=1∧(reverse1 uuu(t)*vvv(t))=reverse1 w))⊃∃t1.(t1>t∧(pc(t1)=2∧vvv(t1)=r%
everse1 w))));
∀E ↑ sub1 nn;
ASSUME n=nn;
REWRITE ↑↑ BY ARITHSS∪NATNUMSS∪{ 23};